equal
deleted
inserted
replaced
15 "-------- distinguish input to I_Model --------------------------------------------------------"; |
15 "-------- distinguish input to I_Model --------------------------------------------------------"; |
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 ("Input_Descript.una", [])])) = @{term "relations"}; |
20 Type e(\<^type_name>\<open>una\<close>, [])])) = @{term "relations"}; |
21 atomtyp (type_of t); |
21 atomtyp (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 |