equal
deleted
inserted
replaced
16 "-------- distinguish input to I_Model --------------------------------------------------------"; |
16 "-------- distinguish input to I_Model --------------------------------------------------------"; |
17 "----- fun Input_Descript.for_bool_list -----"; |
17 "----- fun Input_Descript.for_bool_list -----"; |
18 val t as Const (\<^const_name>\<open>Input_Descript.relations\<close>, |
18 val t as Const (\<^const_name>\<open>Input_Descript.relations\<close>, |
19 Type (\<^type_name>\<open>fun\<close>, [Type (\<^type_name>\<open>list\<close>, [Type (\<^type_name>\<open>bool\<close>,[])]), |
19 Type (\<^type_name>\<open>fun\<close>, [Type (\<^type_name>\<open>list\<close>, [Type (\<^type_name>\<open>bool\<close>,[])]), |
20 Type e(\<^type_name>\<open>una\<close>, [])])) = @{term "relations"}; |
20 Type e(\<^type_name>\<open>una\<close>, [])])) = @{term "relations"}; |
21 atomtyp (type_of t); |
21 TermC.atom_typ @{context} (type_of t); |
22 if Input_Descript.for_bool_list t then () else error "Input_Descript.for_bool_list changed"; |
22 if Input_Descript.for_bool_list t then () else error "Input_Descript.for_bool_list changed"; |
23 "----- fun Input_Descript.for_real -----"; |
23 "----- fun Input_Descript.for_real -----"; |
24 if not (Input_Descript.for_real t) then () else error "Input_Descript.for_real changed"; |
24 if not (Input_Descript.for_real t) then () else error "Input_Descript.for_real changed"; |
25 |
25 |
26 "----- fun is_list_dsc -----"; |
26 "----- fun is_list_dsc -----"; |